Nuprl Lemma : append_rel_wf
4,23
postcript
pdf
T
:Type,
L1
,
L2
,
L
:
T
List. append_rel(
T
;
L1
;
L2
;
L
)
Prop
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
as
@
bs
,
Prop
,
append_rel(
T
;
L1
;
L2
;
L
)
Lemmas
append
wf
origin
T:Type, L1, L2, L:T List. append_rel(T;L1;L2;L) 
Prop T:Type, L1, L2, L:T List. append_rel(T;L1;L2;L) Prop Tx:A. B(x)